(set-option :produce-interpolants 1)
(set-option :certify-interpolants 1)
(set-logic QF_LRA)
(declare-fun |state::state.pc| () Real)
(declare-fun |state::state.old| () Real)
(declare-fun |state::state.new| () Real)
(declare-fun |state::state.ht!5!assimilated| () Bool)
(declare-fun |state::state.ht!4!assimilated| () Bool)
(declare-fun |state::state.ht!3!assimilated| () Bool)
(declare-fun |state::state.ht!2!assimilated| () Bool)
(declare-fun |state::state.ht!1!assimilated| () Bool)
(declare-fun |state::state.ht!0!assimilated| () Bool)
(declare-fun |state::next.ht!0!assimilated| () Bool)
(declare-fun |state::state.ht!5!num_to_migrate| () Real)
(declare-fun |state::state.ht!4!num_to_migrate| () Real)
(declare-fun |state::state.ht!3!num_to_migrate| () Real)
(declare-fun |state::state.ht!2!num_to_migrate| () Real)
(declare-fun |state::state.ht!1!num_to_migrate| () Real)
(declare-fun |state::state.ht!0!num_to_migrate| () Real)
(declare-fun |state::next.ht!0!num_entries| () Real)
(declare-fun |state::state.ht!5!num_entries| () Real)
(declare-fun |state::state.ht!4!num_entries| () Real)
(declare-fun |state::state.ht!3!num_entries| () Real)
(declare-fun |state::state.ht!2!num_entries| () Real)
(declare-fun |state::state.ht!1!num_entries| () Real)
(declare-fun |state::state.ht!0!num_entries| () Real)
(declare-fun |state::next.ht!0!num_to_migrate| () Real)
(declare-fun |state::next.ht!1!assimilated| () Bool)
(declare-fun |state::next.ht!1!num_entries| () Real)
(declare-fun |state::next.ht!1!num_to_migrate| () Real)
(declare-fun |state::next.ht!2!assimilated| () Bool)
(declare-fun |state::next.ht!2!num_entries| () Real)
(declare-fun |state::next.ht!2!num_to_migrate| () Real)
(declare-fun |state::next.ht!3!assimilated| () Bool)
(declare-fun |state::next.ht!3!num_entries| () Real)
(declare-fun |state::next.ht!3!num_to_migrate| () Real)
(declare-fun |state::next.ht!4!assimilated| () Bool)
(declare-fun |state::next.ht!4!num_entries| () Real)
(declare-fun |state::next.ht!4!num_to_migrate| () Real)
(declare-fun |state::next.ht!5!assimilated| () Bool)
(declare-fun |state::next.ht!5!num_entries| () Real)
(declare-fun |state::next.ht!5!num_to_migrate| () Real)
(declare-fun |state::next.pc| () Real)
(declare-fun |state::next.K| () Real)
(declare-fun |state::state.K| () Real)
(declare-fun |state::next.new| () Real)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)

(assert (! (= z (ite (<= 0 x) x (ite (<= 0 y) y (- y))))
:named a))

(assert (! (not (<= 0 z))
:named b))

(check-sat)
(get-interpolants a b)
(exit)


